(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(assert (exists ((q0 Bool) (q1 Bool) (q2 Bool)) (not (=> v4 q0))))
(assert (forall ((q3 Bool)) v2))
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const v20 Bool)
(assert (forall ((q4 Bool) (q5 Bool) (q6 Bool) (q7 Bool)) v16))
(assert (not (forall ((q8 Bool) (q9 Bool) (q10 Bool)) (not (not (=> v0 v10))))))
(declare-const v21 Bool)
(declare-const v22 Bool)
(assert (exists ((q11 Bool) (q12 Bool) (q13 Bool)) v21))
(assert (or (forall ((q11 Bool) (q12 Bool) (q13 Bool)) v15) (exists ((q11 Bool) (q12 Bool) (q13 Bool)) (not (and q13 q13 q13 q12 v11 q13 v22 q12 q13)))))
(assert (or (= v0 v20 v8 v14 v8 v3 (or v8 v3 v16) v9) v0))
(assert (or v16 v11))
(assert (or v9 v21))
(assert (or v11))
(assert (or v5))
(assert (or (= v0 v20 v8 v14 v8 v3 (or v8 v3 v16) v9) v1))
(assert (or (=> v0 v10) v1 v12 v9 v16 v12))
(assert (or v5))
(assert (or v17))
(assert (or v12 v1))
(assert (or v19 v20 (or v8 v3 v16) (=> v0 v10) v0 v17 v12))
(assert (or v12))
(assert (or v9 v9))
(assert (or v21 v3))
(assert (or v3 (=> v0 v10) v11))
(assert (or v5 (=> v0 v10) v2))
(assert (or v21 v0 v3 v11 v1))
(assert (or (or v8 v3 v16)))
(assert (or (=> v0 v10)))
(check-sat)
